module TPFPL where 

import List
import EPLIH

type Subst = [(Var,Term)]

epsilon :: Subst
epsilon = []

cleanUp :: Subst -> Subst
cleanUp = filter (\ (x,x') -> x' /= (Vari x))

dom :: Subst -> [Var]
dom = map fst

rng :: Subst -> [Term]
rng = map snd 

appVar :: Subst -> Var -> Term
appVar []          y               = (Vari y)
appVar ((x,x'):xs) y | x == y      = x'
                     | otherwise   = appVar xs y 

appT :: Subst -> Term -> Term
appT b (Vari y)      = appVar b y
appT b (Struct n ts) = Struct n (appTs b ts) 

appTs :: Subst -> [Term] -> [Term]
appTs = map . appT

appF :: Subst -> Form -> Form 
appF b (Atom a ts)        = Atom a (appTs b ts)
appF b (Neg form)         = Neg (appF b form)
appF b (Impl form1 form2) = Impl (appF b form1) (appF b form2) 
appF b (Equi form1 form2) = Equi (appF b form1) (appF b form2) 
appF b (Conj forms)       = Conj (appFs b forms)
appF b (Disj forms)       = Disj (appFs b forms)
appF b (Forall v form)    = Forall v (appF b' form) 
                            where b' = filter (\ (x,x') -> x /= v) b
appF b (Exists v form)    = Exists v (appF b' form) 
                            where b' = filter (\ (x,x') -> x /= v) b

appFs :: Subst -> [Form] -> [Form]
appFs b = map (appF b)

compose :: Subst -> Subst -> Subst 
compose xs ys = 
  (cleanUp [ (y,(appT xs y')) | (y,y') <-  ys ])
   ++
  (filter (\ (x,x') -> x `notElem` (dom ys)) xs)

unifyTs :: Term -> Term -> [Subst]
unifyTs (Vari x)       (Vari y)       =
        if x==y then [epsilon] else [[(x,Vari y)]]
unifyTs (Vari x)       t2            = 
        [ [(x,t2)] | x `notElem` varsInTerm t2 ]
unifyTs t1            (Vari y)       = 
        [ [(y,t1)] | y `notElem` varsInTerm t1 ]
unifyTs (Struct a ts) (Struct b rs) = 
        [ u | a==b, u <- unifyTlists ts rs ]

unifyTlists :: [Term] -> [Term] -> [Subst]
unifyTlists []     []     = [epsilon]
unifyTlists []     (r:rs) = []
unifyTlists (t:ts) []     = []
unifyTlists (t:ts) (r:rs) = 
   [ (compose sigma2 sigma1) | sigma1 <- unifyTs t r,
                               sigma2 <- unifyTlists (appTs sigma1 ts) 
                                                     (appTs sigma1 rs) ]

skolem ::  Int -> [Var] -> Term
skolem k vs = Struct ("sk" ++ (show k)) [ (Vari x) | x <- vs ]

sk :: Form -> Form
sk f = fst (skf f [] True 0) 

skf :: Form -> [Var] -> Bool -> Int -> (Form,Int)
skf (Atom n ts) vs pol k = ((Atom n ts),k)
skf (Conj fs) vs pol k = ((Conj fs'),j) 
      where (fs',j) = skfs fs vs pol k 
skf (Disj fs) vs pol k = ((Disj fs'),j) 
      where (fs',j) = skfs fs vs pol k 
skf (Forall x f) vs True k = ((Forall x f'),j) 
     where (f',j) = skf f vs' True k 
           vs'   = insert x vs
skf (Forall x f) vs False k = skf (appF b f) vs False (k+1)
     where b = [(x,(skolem k vs))]
skf (Exists x f) vs True k = skf (appF b f) vs True (k+1) 
     where b = [(x,(skolem k vs))]
skf (Exists x f) vs False k = ((Exists x f'),j) 
     where (f',j) = skf f vs' False k 
           vs'   = insert x vs
skf (Neg f) vs pol k = ((Neg f'),j)
     where (f',j) = skf f vs (not pol) k 

skfs :: [Form] -> [Var] -> Bool -> Int -> ([Form],Int)
skfs []     _   _   k  = ([],k)
skfs (f:fs) vs pol k  = ((f':fs'),j) 
   where 
   (f', j1) = skf  f  vs pol k
   (fs',j)  = skfs fs vs pol j1 

p      = Atom "p" 
q      = Atom "q" 
r      = Atom "r" 

refl     = Forall x (r [tx,tx])
irrefl   = Forall x (Neg (r [tx,tx]))
trans    = Forall x0 (Forall x1 (Forall x2 
           (Disj [Neg (r [tx0,tx1]),Neg (r [tx1,tx2]),r [tx0,tx2]])))
ctrans   = Forall x0 (Forall x1 (Forall x2 
           (Disj [r [tx0,tx1], r [tx1,tx2],Neg (r [tx0,tx2])])))
symm     = Forall x0 (Forall x1 
           (Disj [Neg  (r [tx0,tx1]), r [tx1,tx0]]))
asymm    = Forall x0 (Forall x1 
           (Disj [Neg  (r [tx0,tx1]), Neg (r [tx1,tx0])]))
serial   = Forall x0 (Exists x1 (r [tx0,tx1]))
serial1  = Forall x0 (Forall x1 (Exists x2 (r [tx0,tx1,tx2])))
serial2  = Forall x0 (Exists x1 (Exists x2 (r [tx0,tx1,tx2])))
relprop1 = Disj [(Neg asymm),irrefl]
relprop2 = Disj [(Neg trans),(Neg irrefl),asymm]
relprop3 = Disj [(Neg trans),(Neg symm),(Neg serial),refl]

type Index = [Int]

data Node  = Nd Index [Term] [Term] [Form] deriving Show

type Tableau = [Node]

alpha :: Form -> Bool
alpha (Conj _)       = True
alpha (Neg (Disj _)) = True
alpha _              = False 

beta :: Form -> Bool
beta (Disj _)       = True
beta (Neg (Conj _)) = True
beta _              = False

gamma :: Form -> Bool
gamma (Forall _ _)       = True
gamma (Neg (Exists _ _)) = True
gamma _                  = False

plit, nlit, dneg :: Form -> Bool
plit (Atom n ts)       = True 
plit _                 = False
nlit (Neg (Atom n ts)) = True 
nlit _                 = False 
dneg (Neg (Neg f))     = True
dneg _                 = False 

f2t :: Form -> Term
f2t (Atom n ts)       = Struct n ts
f2t (Neg (Atom n ts)) = Struct n ts

components :: Form -> [Form]
components (Conj fs)          = fs
components (Disj fs)          = fs 
components (Neg (Conj fs))    = map (\ f -> Neg f) fs
components (Neg (Disj fs))    = map (\ f -> Neg f) fs
components (Neg (Neg f))      = [f]
components (Forall x f)       = [f]
components (Neg (Exists x f)) = [Neg f]

binder :: Form -> Var
binder (Forall x f)       = x 
binder (Neg (Exists x f)) = x 

decompose :: Form -> ([Var],Form)
decompose form = decomp [] form where 
  decomp xs f = if gamma f then decomp (xs ++ [x]) f' else (xs,f) 
      where x    = binder f
            [f'] = components f

step :: Node  -> Tableau 
step (Nd i pos neg []) = [Nd i pos neg []]
step (Nd i pos neg (f:fs)) 
  | plit  f = if elem (f2t f) neg 
              then [] else [Nd i ((f2t f):pos) neg fs]
  | nlit  f = if elem (f2t f) pos
              then [] else [Nd i pos ((f2t f):neg) fs]
  | dneg  f = [Nd i pos neg ((components f) ++ fs)]
  | alpha f = [Nd i pos neg ((components f) ++ fs)]
  | beta  f = [(Nd (i++[n]) pos neg (f':fs)) |
                          (f',n)   <- zip (components f) [0..] ]
  | gamma f = [Nd i pos neg  (f':(fs++[f]))]
    where 
    (xs,g) = decompose f 
    b      = [((Var j), Vari (Var i)) | (Var j) <- xs ]
    f'     = appF b g

stepD :: Int -> Node -> (Int,Tableau)
stepD k node@(Nd i pos neg []) = (k,[Nd i pos neg []])
stepD k (Nd i pos neg (f:fs))
  | plit  f = if elem (f2t f) neg 
              then (k,[]) else (k,[Nd i ((f2t f):pos) neg fs])
  | nlit  f = if elem (f2t f) pos 
              then (k,[]) else (k,[Nd i pos ((f2t f):neg) fs])
  | dneg  f = (k,[Nd i pos neg ((components f) ++ fs)])
  | alpha f = (k,[Nd i pos neg ((components f) ++ fs)])
  | beta  f = (k,[(Nd (i++[n]) pos neg (f':fs)) |
                          (f',n)   <- zip (components f) [0..] ])
  | gamma f = (k-1,[Nd i pos neg  (f':(fs++[f]))])
    where 
    (xs,g) = decompose f 
    b      = [((Var j), Vari (Var i)) | (Var j) <- xs ]
    f'     = appF b g

expanded :: Node -> Bool 
expanded (Nd i pos neg []) = True
expanded  _                = False

expand :: Int -> Tableau -> Tableau 
expand 0 tableau = tableau 
expand _ []      = []
expand n (node:nodes) = if expanded node 
                       then (node:(expand n nodes))
                       else if k == n 
                       then expand n     (newnodes ++ nodes)
                       else expand (n-1) (nodes ++ newnodes) 
    where (k,newnodes) = stepD n node

checkN :: Node -> [Subst]
checkN (Nd _ pos neg _) = 
   concat [ unifyTs p n | p <- pos, n <- neg ]

appNd :: Subst -> Node -> Node 
appNd b (Nd i pos neg forms) = 
  Nd i (appTs b pos) (appTs b neg) (appFs b forms)

appTab :: Subst -> Tableau -> Tableau
appTab = map . appNd

checkT :: Tableau -> [Subst]
checkT []           = [epsilon]
checkT [node]       = checkN node
checkT (node:nodes) = 
  concat [ checkT (appTab s nodes) | s <- checkN node ]

initTab :: Form -> Tableau 
initTab form = [Nd [] [] [] [form]]

refuteDepth :: Int -> Form -> Bool
refuteDepth k form = checkT tableau /= []
   where tableau = expand k (initTab form)

thm :: Int -> Form -> Bool
thm n = (refuteDepth n) . sk . Neg

sat :: Int -> Form -> Bool
sat n = not . (refuteDepth n) . sk

formula = Disj [Neg trans, Neg symm, Neg serial, refl]

